FDL - Nuprl Lemma : es-knows-trans

Nuprl Lemma : es-knows-trans

poss:(ES{i}

{i'}), R:(possible-event{i:l}(poss)

possible-event{i:l}(poss)

{i'}), P,

Q:(possible-event{i:l}(poss)

{i'}).
(

e:possible-event{i:l}(poss). (P(e))

(Q(e)))

(

e:possible-event{i:l}

(

e:possible-event(poss).

es-knows{i:l}(poss; R; P; e)

es-knows{i:l}(poss; R; Q; e))

Definitions t T, P Q, x:A. B(x), x:A B(x), PossibleEvent(poss), f(a), Type, , ES, x:AB(x), K(P)@e

Lemmas possible-event wf, event system wf